((v3 v1 8) (v4 v1 1) (v3 v4 5) (v4 v2 5))
42
()